Inference at * 1 0 
Iof proof for Lemma lt int eq false elim:



1. i : 
2. j : 
3. i <z j = ff
  (i < j) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 1:n, 4:n, 2:n, 5:n, 6:n, 7:n, 8:n, 9:n, 7:n, 6:n, 10:n} 

latex

 1: .....wf..... NILNIL

 1:   (i <z j = ff)  
 2: .....wf..... NILNIL

 2:   (j z i)  
 3: .....wf..... NILNIL

 3:   (j  i)  
 4: .....wf..... NILNIL

 4:   ((i <z j))  
 5: .....wf..... NILNIL

 5:   i <z j  
 6: .....wf..... NILNIL

 6:   i  
 7: .....wf..... NILNIL

 7:   j  
 8: .....antecedent..... NILNIL

 8:   True
 9: .....wf..... NILNIL

 9: 4. ((i <z j)) = (j z i)
 9:    = 
 10: 

 10: 3. j  i
 10:   (i < j)
 .

Definitions	x:A  B(x), #$n, {x:A| B(x)} , Ax, x.A(x), Type, b, i z j, b, f(a), x:AB(x), A  B, a < b, A, ff, i <z j, , s = t, , , x:A. B(x), P  Q, P & Q, True, T, t  T, P  Q, P  Q
Lemmas	assert of le int, bnot of lt int, bool wf, true wf, squash wf, assert wf, eqff to assert, iff transitivity